package ch.epfl.lara.matcheck.verify.spec;

import ch.epfl.lara.matcheck.ast._

object DomainDeclarationSimplifier {
  
  def apply(f: Formula): Formula = f match {
    case And(left,right) => And(this(left),this(right)) 
    case Or(left,right) => Or(this(left),this(right))
    case EqSet(left,right) => this(And(SubsetEq(left,right),SubsetEq(right,left)))
    case s: SubsetEq => this(s)
    case Tru => Tru
    case Flse => Flse
    case _ => throw new Exception("Unexpected formula")
  }
  
  def apply(a: SubsetEq): Atom = a match {
    case SubsetEq(left,right) => SubsetEq(this(left),this(right))
  }
  
  def apply(s: SetExpr): SetExpr = s match {
    case Union(EmptySet,EmptySet) => EmptySet
    case Union(EmptySet,right) => this(right)
    case Union(left,EmptySet) => this(left)
    case Union(left,right) => Union(this(left),this(right))
    case Intersection(EmptySet,EmptySet) => EmptySet
    case Intersection(EmptySet,right) => EmptySet
    case Intersection(left,EmptySet) => EmptySet
    case Intersection(left,right) => Intersection(this(left),this(right))
    case set @ _ => set
  }
  

}
